(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (< (str.indexof (str.at var1 var3) (str.substr var1 var4 var4) (str.indexof var0 var1 var3)) (str.len (str.at "r7[y8(,7\\k" var3))))
(assert (<= var3 var5))
(assert (<= var3 var5))
(assert (str.prefixof (str.substr (str.substr var1 var3 var3) (str.indexof "4I#VDJL""^D" var1 var3) (str.indexof var1 var2 var4)) (str.substr (str.at var0 8) (str.indexof var0 var1 var4) (str.indexof var1 var2 var3))))
(check-sat)
